This paper presents an efficient, combined formulation of two widely usedabstraction methods for bit-level verification: counterexample-basedabstraction (CBA) and proof-based abstraction (PBA). Unlike previous work, thisnew method is formulated as a single, incremental SAT-problem, interleaving CBAand PBA to develop the abstraction in a bottom-up fashion. It is argued thatthe new method is simpler conceptually and implementation-wise than previousapproaches. As an added bonus, proof-logging is not required for the PBA part,which allows for a wider set of SAT-solvers to be used.
展开▼
